package tr.edu.ege.kipler.satisfiability.syntactical;

import tr.edu.ege.kipler.satisfiability.container.UnfoldableTBox;
import tr.edu.ege.kipler.syntax.atomicformula.ConceptDefinition;
import tr.edu.ege.kipler.syntax.atomicformula.ConceptDefinition.Type;
import tr.edu.ege.kipler.syntax.concept.BinaryConcept;
import tr.edu.ege.kipler.syntax.concept.Concept;
import tr.edu.ege.kipler.syntax.concept.ConceptName;
import tr.edu.ege.kipler.syntax.concept.ConceptVisitor;
import tr.edu.ege.kipler.syntax.concept.ModalConcept;
import tr.edu.ege.kipler.syntax.concept.Nominal;
import tr.edu.ege.kipler.syntax.concept.QualifiedNoRestriction;
import tr.edu.ege.kipler.syntax.concept.RoleQuantification;
import tr.edu.ege.kipler.syntax.concept.BinaryConcept.Constructor;

/**
 * 
 * @author İnanç Seylan
 *
 */
public class UnfoldingVisitor implements ConceptVisitor {
	private Concept result;

	private UnfoldableTBox tbox;

	public UnfoldingVisitor(UnfoldableTBox tbox) {
		this.tbox = tbox;
	}

	public Concept getResult() {
		return result;
	}

	private void setResult(Concept result) {
		this.result = result;
	}

	public void visitBinaryConcept(BinaryConcept bd) {
		BinaryConcept newBd = bd.copy();
		UnfoldingVisitor visitor = new UnfoldingVisitor(tbox);
		bd.getLhs().accept(visitor);
		newBd.setLhs(visitor.getResult());
		visitor = new UnfoldingVisitor(tbox);
		bd.getRhs().accept(visitor);
		newBd.setRhs(visitor.getResult());
		setResult(newBd);
	}

	public void visitConceptName(ConceptName c) {
		setResult(c);
		ConceptName posC = c.copy();
		if (c.isNegated()) {
			posC.toggleNegated();
		}
		ConceptDefinition conDef = tbox.getDefinition(posC);
		if (conDef != null) {
			conDef = eliminatePrimitiveDef(conDef);
			UnfoldingVisitor visitor = new UnfoldingVisitor(tbox);
			conDef.getRhs().accept(visitor);
			Concept result = visitor.getResult();
			if (c.isNegated()) {
				result = result.copy().toggleNegated();
			}
			setResult(result);
		}
	}

	public void visitModalConcept(ModalConcept md) {
		// TODO: think about this
	}

	public void visitQualifiedNoRestriction(QualifiedNoRestriction restriction) {
		QualifiedNoRestriction newRest = restriction.copy();
		UnfoldingVisitor visitor = new UnfoldingVisitor(tbox);
		restriction.getConcept().accept(visitor);
		newRest.setConcept(visitor.getResult());
		setResult(newRest);
	}

	public void visitRoleQuantification(RoleQuantification restriction) {
		RoleQuantification newRest = restriction.copy();
		UnfoldingVisitor visitor = new UnfoldingVisitor(tbox);
		restriction.getConcept().accept(visitor);
		newRest.setConcept(visitor.getResult());
		setResult(newRest);
	}

	public void visitNominal(Nominal nominal) {
		// TODO Auto-generated method stub
		
	}

	private ConceptDefinition eliminatePrimitiveDef(ConceptDefinition cd) {
		ConceptDefinition result;
		if (cd.getType() == Type.PRIMITIVE) {
			ConceptName c = (ConceptName) cd.getLhs();
			ConceptName newC = new ConceptName(c.getName() + "'");
			result = new ConceptDefinition(Type.NON_PRIMITIVE, cd.getLhs(),
					new BinaryConcept(Constructor.INTERSECTION, newC, cd
							.getRhs()));
		} else {
			result = cd;
		}
		return result;
	}

}
